$\forall$$A$:Type, $d_{1}$, $d_{2}$:EqDecider($A$), $f$:$a$:$A$ fp$\rightarrow$ Type, $x$:$A$, $z$:Type. $f$($x$)?$z$ $\subseteq\rho$ $f$($x$)?$z$